0 CpxTRS
↳1 RenamingProof (⇔, 0 ms)
↳2 CpxRelTRS
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 typed CpxTrs
↳5 OrderProof (LOWER BOUND(ID), 0 ms)
↳6 typed CpxTrs
↳7 RewriteLemmaProof (LOWER BOUND(ID), 450 ms)
↳8 BEST
↳9 typed CpxTrs
↳10 RewriteLemmaProof (LOWER BOUND(ID), 440 ms)
↳11 BEST
↳12 typed CpxTrs
↳13 LowerBoundsProof (⇔, 0 ms)
↳14 BOUNDS(n^2, INF)
↳15 typed CpxTrs
↳16 LowerBoundsProof (⇔, 0 ms)
↳17 BOUNDS(n^2, INF)
↳18 typed CpxTrs
↳19 LowerBoundsProof (⇔, 0 ms)
↳20 BOUNDS(n^1, INF)
isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)
isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0') → s(0')
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0')
They will be analysed ascendingly in the following order:
inc < count
Generator Equations:
gen_empty:node4_0(0) ⇔ empty
gen_empty:node4_0(+(x, 1)) ⇔ node(empty, gen_empty:node4_0(x))
gen_0':s5_0(0) ⇔ 0'
gen_0':s5_0(+(x, 1)) ⇔ s(gen_0':s5_0(x))
The following defined symbols remain to be analysed:
inc, count
They will be analysed ascendingly in the following order:
inc < count
Induction Base:
inc(gen_0':s5_0(0)) →RΩ(1)
s(0')
Induction Step:
inc(gen_0':s5_0(+(n7_0, 1))) →RΩ(1)
s(inc(gen_0':s5_0(n7_0))) →IH
s(gen_0':s5_0(+(1, c8_0)))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Lemmas:
inc(gen_0':s5_0(n7_0)) → gen_0':s5_0(+(1, n7_0)), rt ∈ Ω(1 + n70)
Generator Equations:
gen_empty:node4_0(0) ⇔ empty
gen_empty:node4_0(+(x, 1)) ⇔ node(empty, gen_empty:node4_0(x))
gen_0':s5_0(0) ⇔ 0'
gen_0':s5_0(+(x, 1)) ⇔ s(gen_0':s5_0(x))
The following defined symbols remain to be analysed:
count
Induction Base:
count(gen_empty:node4_0(0), gen_0':s5_0(b)) →RΩ(1)
if(isEmpty(gen_empty:node4_0(0)), isEmpty(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)), node(left(left(gen_empty:node4_0(0))), node(right(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, isEmpty(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)), node(left(left(gen_empty:node4_0(0))), node(right(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, isEmpty(empty), right(gen_empty:node4_0(0)), node(left(left(gen_empty:node4_0(0))), node(right(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, true, right(gen_empty:node4_0(0)), node(left(left(gen_empty:node4_0(0))), node(right(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, true, empty, node(left(left(gen_empty:node4_0(0))), node(right(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, true, empty, node(left(empty), node(right(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, true, empty, node(empty, node(right(left(gen_empty:node4_0(0))), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, true, empty, node(empty, node(right(empty), right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, true, empty, node(empty, node(empty, right(gen_empty:node4_0(0)))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(true, true, empty, node(empty, node(empty, empty)), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →LΩ(1 + b)
if(true, true, empty, node(empty, node(empty, empty)), gen_0':s5_0(b), gen_0':s5_0(+(1, b))) →RΩ(1)
gen_0':s5_0(b)
Induction Step:
count(gen_empty:node4_0(+(n291_0, 1)), gen_0':s5_0(b)) →RΩ(1)
if(isEmpty(gen_empty:node4_0(+(n291_0, 1))), isEmpty(left(gen_empty:node4_0(+(n291_0, 1)))), right(gen_empty:node4_0(+(n291_0, 1))), node(left(left(gen_empty:node4_0(+(n291_0, 1)))), node(right(left(gen_empty:node4_0(+(n291_0, 1)))), right(gen_empty:node4_0(+(n291_0, 1))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, isEmpty(left(gen_empty:node4_0(+(1, n291_0)))), right(gen_empty:node4_0(+(1, n291_0))), node(left(left(gen_empty:node4_0(+(1, n291_0)))), node(right(left(gen_empty:node4_0(+(1, n291_0)))), right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, isEmpty(empty), right(gen_empty:node4_0(+(1, n291_0))), node(left(left(gen_empty:node4_0(+(1, n291_0)))), node(right(left(gen_empty:node4_0(+(1, n291_0)))), right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, true, right(gen_empty:node4_0(+(1, n291_0))), node(left(left(gen_empty:node4_0(+(1, n291_0)))), node(right(left(gen_empty:node4_0(+(1, n291_0)))), right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, true, gen_empty:node4_0(n291_0), node(left(left(gen_empty:node4_0(+(1, n291_0)))), node(right(left(gen_empty:node4_0(+(1, n291_0)))), right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, true, gen_empty:node4_0(n291_0), node(left(empty), node(right(left(gen_empty:node4_0(+(1, n291_0)))), right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, true, gen_empty:node4_0(n291_0), node(empty, node(right(left(gen_empty:node4_0(+(1, n291_0)))), right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, true, gen_empty:node4_0(n291_0), node(empty, node(right(empty), right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, true, gen_empty:node4_0(n291_0), node(empty, node(empty, right(gen_empty:node4_0(+(1, n291_0))))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →RΩ(1)
if(false, true, gen_empty:node4_0(n291_0), node(empty, node(empty, gen_empty:node4_0(n291_0))), gen_0':s5_0(b), inc(gen_0':s5_0(b))) →LΩ(1 + b)
if(false, true, gen_empty:node4_0(n291_0), node(empty, node(empty, gen_empty:node4_0(n291_0))), gen_0':s5_0(b), gen_0':s5_0(+(1, b))) →RΩ(1)
count(gen_empty:node4_0(n291_0), gen_0':s5_0(+(1, b))) →IH
gen_0':s5_0(+(+(1, b), c292_0))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Lemmas:
inc(gen_0':s5_0(n7_0)) → gen_0':s5_0(+(1, n7_0)), rt ∈ Ω(1 + n70)
count(gen_empty:node4_0(n291_0), gen_0':s5_0(b)) → gen_0':s5_0(+(n291_0, b)), rt ∈ Ω(1 + b + b·n2910 + n2910)
Generator Equations:
gen_empty:node4_0(0) ⇔ empty
gen_empty:node4_0(+(x, 1)) ⇔ node(empty, gen_empty:node4_0(x))
gen_0':s5_0(0) ⇔ 0'
gen_0':s5_0(+(x, 1)) ⇔ s(gen_0':s5_0(x))
No more defined symbols left to analyse.
Lemmas:
inc(gen_0':s5_0(n7_0)) → gen_0':s5_0(+(1, n7_0)), rt ∈ Ω(1 + n70)
count(gen_empty:node4_0(n291_0), gen_0':s5_0(b)) → gen_0':s5_0(+(n291_0, b)), rt ∈ Ω(1 + b + b·n2910 + n2910)
Generator Equations:
gen_empty:node4_0(0) ⇔ empty
gen_empty:node4_0(+(x, 1)) ⇔ node(empty, gen_empty:node4_0(x))
gen_0':s5_0(0) ⇔ 0'
gen_0':s5_0(+(x, 1)) ⇔ s(gen_0':s5_0(x))
No more defined symbols left to analyse.
Lemmas:
inc(gen_0':s5_0(n7_0)) → gen_0':s5_0(+(1, n7_0)), rt ∈ Ω(1 + n70)
Generator Equations:
gen_empty:node4_0(0) ⇔ empty
gen_empty:node4_0(+(x, 1)) ⇔ node(empty, gen_empty:node4_0(x))
gen_0':s5_0(0) ⇔ 0'
gen_0':s5_0(+(x, 1)) ⇔ s(gen_0':s5_0(x))
No more defined symbols left to analyse.